The present invention relates to a method and a system for verifying properties of a computer program.
It applies notably to all computer programs in the form of source codes whose properties, notably dependability, security and proper operation, one wishes to verify. It applies in particular in respect of critical computer programs.
There exist critical computer programs embedded for example in aerial and terrestrial transports and nuclear facilities. It is necessary, indeed obligatory, to ensure that these programs comply notably with properties of dependability, security and proper operation. Other properties can be verified. These properties are expressed on the source code of the program investigated.
Several procedures can be used to provide elements of confidence in critical programs by verifying properties about their source code. Two types of procedures are particularly known, test procedures and static analysis procedures.
Test procedures involve executing the program on a large number of inputs. As there are too many different inputs, some of them are selected, hoping that these are representative of all the behaviours of the program. These procedures may therefore afford only partial confidence in the program.
Static analysis procedures involve investigating the source code without executing it. Various static analysis procedures exist and provide guarantees about the behaviour of the program for all its inputs. In general this problem has no solution: it forms part of the class of undecidable problems. The existing procedures must therefore proceed by approximations. These approximations can be of two kinds: either they make it possible to give a subset comprising only definite errors, or they make it possible to give a super-set of potential errors. In the first case, the effect of the approximation is that certain errors may be omitted. In the second case, the analysis may indicate errors that the source code does not actually exhibit. Within the framework of the analysis of a critical code, consideration is generally given to the second family of approximations so as to have the possibility of being certain that no error remains in the source program investigated. Moreover, static analysis relies on formal modelling of the language used in the source program investigated. This modelling may not take into account certain aspects of the language for technical reasons. Because of these choices in the modelling, a given static analysis procedure may be incapable of processing certain parts of the source program to be investigated.